PR summary 4b3db1614d

Import changes for modified files

No significant changes to the import graph

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

This pull request has conflicts, please merge master and resolve them.

After some discussion with Andrew, the following is my suggestion for this PR:

• Define a pushforward for Function.locallyFinsupp for prespectral and sober topological spaces taking a weight function as an argument X → R, which is what replaces the mapAux (the proof might require some more topological assumptions, of which we can of course assume the ones that are true in the application).
• Given s : Set X, t : Set Y and a Function.locallyFinsupp with support in s, there should be a lemma showing that, under some compatibility with the weights, the image of the pushforward has support in t.
• This will then induce a map between the "homogeneous cycles", which is just the additive submonoid of cycles with support in a given set.

In the next PR, I would suggest to:

• Add the abbrev for AlgebraicCycle as it is done here.
• Define the weights function for a morphism of schemes as you do here, but make it Nat-valued. This will still allow to apply the above construction by coercing the Nats to elements of the coefficient ring.
• Remove Grading and HasDegree.

This pull request has conflicts, please merge master and resolve them.

This PR/issue depends on:

• [Merged by Bors] - feat(AlgebraicGeometry): Add some minimal API for orders on schemes #26225
• [Merged by Bors] - feat(Topology): Connecting different notions of locally finite #26259
• [Merged by Bors] - chore(Topology): Generalised some of the instances for Function.locallyFinsuppWithin  #35807
  By Dependent Issues (🤖). Happy coding!

After some discussion with Andrew, the following is my suggestion for this PR:

• Define a pushforward for Function.locallyFinsupp for prespectral and sober topological spaces taking a weight function as an argument X → R, which is what replaces the mapAux (the proof might require some more topological assumptions, of which we can of course assume the ones that are true in the application).
• Given s : Set X, t : Set Y and a Function.locallyFinsupp with support in s, there should be a lemma showing that, under some compatibility with the weights, the image of the pushforward has support in t.
• This will then induce a map between the "homogeneous cycles", which is just the additive submonoid of cycles with support in a given set.

In the next PR, I would suggest to:

• Add the abbrev for AlgebraicCycle as it is done here.
• Define the weights function for a morphism of schemes as you do here, but make it Nat-valued. This will still allow to apply the above construction by coercing the Nats to elements of the coefficient ring.
• Remove Grading and HasDegree.

What's here I think fulfils this, but I now think it's probably more sensible design-wise to directly use Function.locallyFinsuppWithin to talk about locally finsupp functions with support in s. I'm temporarily making this PR WIP to try and do such a refactor.

Edit: Christian already knows this, but for anyone else who happens to be reading this, we realised this idea does not quite work so I've reverted this to the state it was in before I attempted the refactor and have removed the WIP label

🚀 Pull request has been placed on the maintainer queue by chrisflav.

@joelriou can you have a final look?

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job